Step of Proof: nat_well_founded
9,38
postcript
pdf
Inference at
*
1
I
of proof for Lemma
nat
well
founded
:
P
:(
). (
j
:
. (
k
:
. (
k
<
j
)
P
(
k
))
P
(
j
))
{
n
:
.
P
(
n
)}
latex
by ((RepD)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C
)) (first_tok :t) inil_term)))
latex
C
1
:
C1:
1.
P
:
C1:
2.
j
:
. (
k
:
. (
k
<
j
)
P
(
k
))
P
(
j
)
C1:
n
:
.
P
(
n
)
C
.
Definitions
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
Lemmas
nat
wf
origin